package logica;

import java.util.ArrayList;
import java.util.List;
import java.util.Map;

import util.Tupla;

public class CalculoProposicional 
{
	/** Conjunto alfa padrão. Contem todas as letras de A a Z maiúsculas. */
	public static final Character[] 
		CONJUNTO_ALFA_PADRAO = {'A', 'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K',
			'L', 'M', 'N', 'O', 'P', 'Q', 'R', 'S', 'T', 'U', 'V', 'W', 'X', 'Y', 'Z'};
	
	/** Conjunto de caracteres validos como atomos neste cálculo proposicional. */
	private Character[] conjuntoAlfa = CONJUNTO_ALFA_PADRAO;
				
	private enum TipoDeFormula
	{
		NEGACAO, CONJUNCAO, DISJUNCAO, IMPLICACAO, EQUIVALENCIA, ATOMO
	}
	
	/** Conjunto omega padrão.
	 *<br> ¬ negacao
	 *<br> ^ conjuncao
	 *<br> v disjuncao
	 *<br> -> implicacao
	 *<br> <-> equivalencia */
	public static final String[] 
			CONJUNTO_OMEGA_PADRAO = {"¬", "^", "v", "->", "<->"};
	
	/** Conjunto de símbolos que representam os operadores.
	 * Os símbolos sempre significam, nessa ordem:
	 *<br> negação		(indice 0) 
	 *<br> conjunção	(indice 1)
	 *<br> disjunção	(indice 2)
	 *<br> implicação	(indice 3)
	 *<br> equivalencia	(indice 4)
	*/
	private String[] conjuntoOmega = CONJUNTO_OMEGA_PADRAO;
	
	
	/** Variável para usar no metodo toString */
	private static String __tab; //so para usar no toString da formula, e evitar um argumento a mais
	
	public class Formula {
		
		/** Termos uma formula. O termo primario é usado na negação. Em atomos, nenhum dos dois é preenchido. */
		private Formula primaria, secundaria;
		
		/** Operacao da formula. */
		private TipoDeFormula operacao;
		
		/** Charactere do átomo, caso a formula seja um átomo. */
		private Character atomo;
		
		
		public Formula(String exp) throws Exception
		{
			Formula f = intepretar(exp);
			this.atomo = f.atomo;
			this.secundaria = f.secundaria;
			this.primaria = f.primaria;
			this.operacao = f.operacao;
		}
		
		public Formula()
		{
			primaria = null;
			secundaria = null;
			operacao = null;
			atomo = null;
		}
		
		private Formula intepretar(String exp) throws Exception
		{
			exp = exp.trim();
			
			if(exp.length() == 0) throw new Exception("Expressão vazia!");
			
			List<Tupla<Formula, TipoDeFormula>> termosAchados = new ArrayList<Tupla<Formula,TipoDeFormula>>();

			while(exp.length() > 0)
			{
				if(comecaComParenteses(exp))
				{
					if(exp.length() < 2) //tem algo mais alem do parentese?
						throw new Exception("Esperado um fecha-parenteses, mas trecho acaba antes! Trecho: \""+exp+"\"");
					
					exp = exp.substring(1).trim(); //pego o que esta logo apos o '('
					try
					{
						int i = indiceFechaParentesisCorrespondente(exp);
						Formula ff = intepretar(exp.substring(0, i)); //interpreta a formula dentro dos parenteses
						exp = exp.substring(i+1).trim(); //pego o que vem depois do ')', sem espaços desnecessarios
						if(exp.length() > 0) //tem algo mais depois de um termo entre parenteses?
						{
							if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
							{
								String operador = operadorBinarioNoIncioDe(exp);
								exp = exp.substring(operador.length());//pego o que vem apos o operador
								termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
								//apos isso, volta para o loop para achar outros termos no mesmo nivel
							}
							else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
						}
						else //exp terminou com uma expressao entre parenteses
							termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
					}
					catch(Exception e)
					{
						throw new Exception("Problema ao procurar fecha-parenteses. Trecho: \""+exp+"\"\n"+e.getMessage());
					}
				}
				
				else if(serAtomo(exp.charAt(0)))
				{
					Formula ff = new Formula();
					ff.atomo = exp.charAt(0);
					ff.operacao = TipoDeFormula.ATOMO;
					exp = exp.substring(1).trim(); //pego o que vem depois do atomo, sem espaços desnecessarios
					
					if(exp.length() > 0) //tem algo mais depois de um atomo?
					{
						if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
						{
							String operador = operadorBinarioNoIncioDe(exp);
							exp = exp.substring(operador.length());//pego o que vem apos o operador
							termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
							//apos isso, volta para o loop para achar outros termos no mesmo nivel
						}
						else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
					}
					else //exp terminou com uma expressao entre parenteses
						termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
				}
				else if(comecaComNegacao(exp))
				{
					Formula ff = new Formula();
					ff.operacao = TipoDeFormula.NEGACAO;
					exp = exp.substring(conjuntoOmega[0].length()); //pula o simbolo de negacao
					int i = indiceProximoOperadorPrecedenciaInferiorANegacao(exp);
					ff.primaria = intepretar(exp.substring(0, i));
					exp = exp.substring(i).trim(); //pego o que vem depois do escopo da negacao, sem espaços desnecessarios
					
					if(exp.length() > 0) //tem algo mais depois do escopo da negacao?
					{
						if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
						{
							String operador = operadorBinarioNoIncioDe(exp);
							exp = exp.substring(operador.length());//pego o que vem apos o operador
							termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
							//apos isso, volta para o loop para achar outros termos no mesmo nivel
						}
						else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
					}
					else //exp terminou com uma expressao entre parenteses
						termosAchados.add(new Tupla<Formula, TipoDeFormula>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
				}
				
				exp = exp.trim();
			}
			
			return arrumaTermosPorPrecedencia(termosAchados);
		}
		
		private boolean comecaComParenteses(String exp)
		{
			return exp.charAt(0) == '(';
		}
		
		private boolean serAtomo(char ch)
		{
			for(char c : conjuntoAlfa)
				if(c == ch) return true;
			return false;
		}
		
		private boolean comecaComOperadorBinario(String exp)
		{
			if(operadorBinarioNoIncioDe(exp) == null) return false;
			else return true;
		}
		
		private TipoDeFormula operacaoCorrespondenteA(String op)
		{
			for(int i = 1; i < conjuntoAlfa.length; i++)
				if(op.equals(conjuntoOmega[i])) switch(i)
				{
					case 1: return TipoDeFormula.CONJUNCAO;
					case 2: return TipoDeFormula.DISJUNCAO;
					case 3: return TipoDeFormula.IMPLICACAO;
					case 4: return TipoDeFormula.EQUIVALENCIA;
					default: return null; //não deveria acontecer
				}
			return null;
		}
		
		private String operadorBinarioNoIncioDe(String exp)
		{
			for(int i = 1; i < conjuntoAlfa.length; i++)
				if(exp.startsWith(conjuntoOmega[i]))
				{
					return conjuntoOmega[i];
				}
			return null;
		}
		
		private boolean comecaComNegacao(String exp)
		{
			return exp.startsWith(conjuntoOmega[0]);
		}
		
		private int indiceProximoOperadorPrecedenciaInferiorANegacao(String exp)
		{
			String str = exp;
			do
			{
				for(int i = 1; i < conjuntoOmega.length; i++)
				{
					if(str.startsWith(conjuntoOmega[i]))
					{
						break;
					}
				}
				if(str.charAt(0) == '(')
				{
					int contaParenteses = 1;
					do
					{
						str = str.substring(1);
						if(str.charAt(0) == '(') contaParenteses++;
						else if(str.charAt(0) == ')') contaParenteses--;
						
					}while(contaParenteses != 0);
					
				}
				str = str.substring(1);
			}
			while(str.length() > 0);
			
			return exp.length()-str.length();
		}
		
		/** Retorna o indice do fecha parenteses correspondente ao nivel atual de escopo. O abre parentese deve estar omitido. 
		 * @throws Exception Quando não acha o parentese correspondente*/
		private int indiceFechaParentesisCorrespondente(String subexp) throws Exception
		{
			int count=0;
			char[] array = subexp.toCharArray();
			for(int i = 0; i < array.length; i++)
			{
				if(array[i] == '(')
					count++;
				
				else if(array[i] == ')')
				{
					if(count == 0) return i;
					else count--;
				}	
			}
			throw new Exception("Indice nao encontrado!");
		}
		
		private Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, TipoDeFormula>> termos) throws Exception
		{
			return arrumaTermosPorPrecedencia(termos, TipoDeFormula.EQUIVALENCIA);
		}
		
		private Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, TipoDeFormula>> termos, TipoDeFormula operacaoPrecedente) throws Exception
		{
			Formula formulaAnterior = null;
			
			if(operacaoPrecedente == TipoDeFormula.CONJUNCAO) // se for conjuncao, ja esta limpo de todos os outros termos menos precedentes
			{
				for(Tupla<Formula, TipoDeFormula> tupla : termos)
				{
					if(formulaAnterior == null)
					{
						formulaAnterior = tupla.termo1;
					}
					else
					{
						Formula f = new Formula();
						f.operacao = TipoDeFormula.CONJUNCAO;
						f.primaria = formulaAnterior;
						f.secundaria = tupla.termo1;
						formulaAnterior = f;
					}
				}
				return formulaAnterior;
			}
			
			//se nao for conjuncao, vamos descobrir que sera o cara mais precedente apos o atual
			TipoDeFormula proximaOperacaoPrecedente = null;
			switch(operacaoPrecedente)
			{
				case EQUIVALENCIA:
					proximaOperacaoPrecedente = TipoDeFormula.IMPLICACAO;
					break;
				case IMPLICACAO:
					proximaOperacaoPrecedente = TipoDeFormula.DISJUNCAO;
					break;
				case DISJUNCAO:
					proximaOperacaoPrecedente = TipoDeFormula.CONJUNCAO;
					break;
				default:
					break;
			}
			
			for(int i = 0, a = 0; i < termos.size(); i++)
			{
				if(termos.get(i).termo2 == operacaoPrecedente)
				{
					List<Tupla<Formula, TipoDeFormula>> sublista = termos.subList(a, i+1);
					sublista.get(i-a).termo2 = null;
					
					Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
					
					if(formulaAnterior == null)
					{
						formulaAnterior = f;
					}
					else
					{
						Formula ff = new Formula();
						ff.operacao = operacaoPrecedente;
						ff.primaria = formulaAnterior;
						ff.secundaria = f;
						formulaAnterior = ff;
					}
					
					a = i+1;
				}
				else if(termos.get(i).termo2 == null) // chegamos no fim da lista de termos, hora de finalizar
				{
					List<Tupla<Formula, TipoDeFormula>> sublista = termos.subList(a, i+1);
					
					Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
					
					if(formulaAnterior == null) // nao teve nenhum termo encotrado antes da operacao
					{
						return f;
					}
					else
					{
						Formula ff = new Formula();
						ff.operacao = operacaoPrecedente;
						ff.primaria = formulaAnterior;
						ff.secundaria = f;
						return ff;
					}
				}
			}
			throw new Exception("Erro ao organizar precedencia!");
		}
		
		@Override
		public String toString()
		{
			__tab = "";
			return this.__toString();
		}

		private String __toString()
		{
			String str="";

			__tab += "-";
			
			if(this.operacao == TipoDeFormula.ATOMO)
			{
				str += "\n"+__tab + this.atomo;
			}
			else if(this.operacao == TipoDeFormula.NEGACAO)
			{
				str += "\n"+__tab + "NEGACAO";
				str += "\n"+__tab + this.primaria.__toString();
			}
			else
			{
				str += "\n"+__tab + this.operacao.name();
				str += this.primaria.__toString();
				str += this.secundaria.__toString();
			}
			
			__tab = __tab.substring(1);
			
			return str;
		}
		
		public boolean valorar(Map<Character, Boolean> valorDosAtomos)
		{
			switch(this.operacao)
			{
				case EQUIVALENCIA:
					return (primaria.valorar(valorDosAtomos) == secundaria.valorar(valorDosAtomos));
				
				case IMPLICACAO:
					return (!primaria.valorar(valorDosAtomos) || secundaria.valorar(valorDosAtomos));
					
				case CONJUNCAO:
					return (primaria.valorar(valorDosAtomos) && secundaria.valorar(valorDosAtomos));
					
				case DISJUNCAO:
					return (primaria.valorar(valorDosAtomos) || secundaria.valorar(valorDosAtomos));
					
				case NEGACAO:
					return !primaria.valorar(valorDosAtomos);
					
				case ATOMO:
					return valorDosAtomos.get(atomo);
				
				default:
					return false;
			}
		}

	}
	
	public static final CalculoProposicional PADRAO = new CalculoProposicional();

	public Character[] getConjuntoAlfa() {
		return conjuntoAlfa;
	}

	public void setConjuntoAlfa(Character[] conjuntoAlfa) {
		this.conjuntoAlfa = conjuntoAlfa;
	}

	public String[] getConjuntoOmega() {
		return conjuntoOmega;
	}

	public void setConjuntoOmega(String[] conjuntoOmega) {
		this.conjuntoOmega = conjuntoOmega;
	}
	

}
